Nuprl Definition : deq
0,22
postcript
pdf
EqDecider(
T
) ==
eq
:(
T
T
)
(
x
,
y
:
T
.
x
=
y
eq
(
x
,
y
))
latex
clarification:
EqDecider(
T
) ==
eq
:(
T
T
)
(
x
:
T
,
y
:
T
.
x
=
y
T
eq
(
x
,
y
))
latex
Definitions
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
,
x
:
A
.
B
(
x
)
,
P
Q
,
s
=
t
,
b
,
f
(
a
)
FDL editor aliases
deq
origin
T
)
(
x, y:T. x = y 
eq(x,y))
T)(x:T, y:T. x = y 
T eq(x,y)) T)(x, y:T. x = y eq(x,y))
T)(x:T, y:T. x = y T eq(x,y)) B(x)B(x)x:A. B(x) Q
b